NIL 
EVAL-AWAITS 
NIL 1 159
1 (SB(A)∩ SB(B))≡ SB((A ∩ B));3 61
3 f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB((A ∩ B))⊃(SB(A)∩ SB(B))≡ SB((A ∩ B));5 6
5 f((SB(A)∩ SB(B)),SB((A ∩ B)))ε(SB(A)∩ SB(B));9 10
6 f(x,y)ε x∧f(x,y)ε y⊃x ≡ y;a1
9 f((SB(A)∩ SB(B)),SB((A ∩ B)))ε x⊃f((SB(A)∩ SB(B)),SB((A ∩ B)))ε(SB(A)∩ x);15 16
10 f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB(B);17 24
15 f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB(A);23 24
16 x ε y∧x ε z⊃x ε(y ∩ z);a3
17 f((SB(A)∩ SB(B)),SB((A ∩ B)))ε U⊃f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB(B);25 92
23 f((SB(A)∩ SB(B)),SB((A ∩ B)))ε U⊃f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB(A);35 92
24 f((SB(A)∩ SB(B)),SB((A ∩ B)))ε U;61 94
25 f((SB(A)∩ SB(B)),SB((A ∩ B)))⊂ B;47 40
35 f((SB(A)∩ SB(B)),SB((A ∩ B)))⊂ A;47 48
40 x ⊂(z ∩ y)⊃x ⊂ y;a5
47 f((SB(A)∩ SB(B)),SB((A ∩ B)))⊂(A ∩ B);61 144
48 x ⊂(y ∩ z)⊃x ⊂ y;a5
61 f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB((A ∩ B));75 76
75 f((SB(A)∩ SB(B)),SB((A ∩ B)))ε U⊃f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB((A ∩ B));91 92
76 f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB((A ∩ B))∨f((SB(A)∩ SB(B)),SB((A ∩ B)))ε U;129 94
91 f((SB(A)∩ SB(B)),SB((A ∩ B)))⊂(A ∩ B)∨f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB((A ∩ B));109 110
92 x ⊂ y∧x ε U⊃x ε SB(y);a7
94 x ε SB(y)⊃x ε U;a7
109 f((SB(A)∩ SB(B)),SB((A ∩ B)))⊂ x⊃f((SB(A)∩ SB(B)),SB((A ∩ B)))⊂(A ∩ x)∨f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB((A ~
∩ B));127 128
110 f((SB(A)∩ SB(B)),SB((A ∩ B)))⊂ B∨f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB((A ∩ B));129 144
127 f((SB(A)∩ SB(B)),SB((A ∩ B)))⊂ A∨f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB((A ∩ B));143 144
128 x ⊂ y∧x ⊂ z⊃x ⊂(y ∩ z);a5
129 f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB((A ∩ B))∨f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB(B);153 146
143 f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB((A ∩ B))∨f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB(A);153 154
144 x ε SB(y)⊃x ⊂ y;a7
146 x ε(z ∩ y)⊃x ε y;a3
153 f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB((A ∩ B))∨f((SB(A)∩ SB(B)),SB((A ∩ B)))ε(SB(A)∩ SB(B));159 160
154 x ε(y ∩ z)⊃x ε y;a3
159 ¬(SB(A)∩ SB(B))≡ SB((A ∩ B));THEOREM
160 x ≡ y∨(f(x,y)ε y∨f(x,y)ε x);a1
NIL 
EVAL-AWAITS